FDL - Step of Proof: comp_nat_ind_tp

Step of Proof: comp_nat_ind_tp

Inference at * 1 1
Iof proof for Lemma comp nat ind tp:

1. P :

{k}
2.

i:

. (

j:

. (j < i)

P(j))

P(i)
3. i :

P(i)

by PushArgs [`hn`,int_to_arg 3]

1:

1:

P(i)

.